es:ES, i:Id, P:(state@iProp).
@i stable state.P(state)    e@i. P((state when e))  e'e.P((state when e')) 

latex

Definitions	x(s), x:A. B(x), t  T, A & B, P  Q, P  Q, P & Q, P  Q, True, b, False, A, (e <loc e'), T, ES, Id, state@i, (state when e), E, e  e' , Prop, {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), loc(e), @i stable state.P(state)  , e@i. P(e), e'e.P(e'), pred(e), P  Q, SQType(T), 1of(t)
Lemmas	Id sq, state-after-pred, es-pred wf, es-pred-locl, es-stable wf, es-loc wf, es-locl-wellfnd, es-locl wf, es-le wf, es-E wf, es-state-when wf, es-state wf, squash wf, true wf, Id wf, event system wf, es-le-loc, es-loc-pred, es-le-iff